open import Function using (_$_ ; _∘_)
open import Data.Product using (∃ ; Σ ; _×_ ; _,_ ; _,′_ ; proj₁ ; proj₂)
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ )
open import Relation.Unary using ( Pred ; U; Decidable ;_∈_ )
open import Relation.Binary using ( _Respects_)
open import Algebra.Structures using (  IsGroup ; IsAbelianGroup ; IsSemigroup ; IsRing )
open import Algebra using ( Group ; Monoid ; Semigroup ; AbelianGroup ; Ring )
open import Level using ( Level ; _⊔_ ; suc )
open import Relation.Binary using ( Rel )
open import Substructures using (IsSubGroup; SubGroup ; IsSubMonoid ; IsSubAbelianGroup; everySubGroupOfAbelianIsNormal )
open import QuotientRelation using (QuotientRelation; quotientGroupIsAGroup)
import Relation.Binary.EqReasoning as EqR
open import Algebra.Morphism
open import Kern using (Kernₕ; kernₕ-induces-subgroup)


module Ideal where

{--
A function f from a ring R to a ring S is a ring homomorphism if it is a homomorphism of the additive groups and homomorphism of the multiplicative monoids. The map from the ring of integers Z to S that takes n to n∙1 is a ring homomorphism. An additive subgroup I of a ring R is an ideal if for each x in I and each r in R the elements rx and xr are in I. I is easily seen that if f is a ring homomorphism then `ker f = f⁻¹(0)` is and ideal. An ideal I is proper if 1 ∉ I.
--}

{--
Ideał się składa z:
* Pierścienia R nad grupą addytywną G i monoidem multiplikatywnym z działaniem ∙ (wyszczególnione bo potrzebne w dalszej części definicji)
* Podgrupy I grupy G
* Dowodu że ∀ (x ∈ I) : ∀ (r ∈ R) : [(r∙x ∈ I)  × (x∙r ∈ I)]
Jeśli ktoś to czyta to zarzucę żarcikiem: Wchodzi gość do cukierni trzymając w jeden ręce szpachlę a w drugiej śrubokręt. I kupuje pączka. I stojąc przy ladzie zaczyna szpachelką i śrubokrętem wyjmować marmoladę z tego pączka. Kasjerska się pyta: "Czy jest pan motocyklistą?". Koleś odpowiada: "Tak, skąd pani wie". Na to ona: "A bo widziałam że przyjechał pan motocyklem".
--}

IdealProp : {a p : Level} {A : Set a} (I : Pred A p) (∙ : Op₂ A) →
  (r : A) →  (x : A) → (_ : I x) → Set p
IdealProp I _∙_ r x ix = ((r ∙ x) ∈ I) × ((x ∙ r) ∈ I)

record IsIdeal {a p ℓ : Level} {A : Set a } (I : Pred A p) (_≈_ : Rel A ℓ) (+ ∙ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ ⊔ p) where
  field
    isRing : IsRing _≈_ + ∙ -_ 0# 1#
    isSubGroup : IsSubGroup _≈_ I + 0# -_
    idealProp : (r : A) {x : A} (ix : I x) → IdealProp I ∙ r x ix
    -- Nie wiedzieć czemu nie kompiluje się bez argumentów wypisanych wprost

  idealˡ : (r : A) {x : A} (ix : I x) → (∙ r x) ∈ I
  idealˡ r {x} ix = proj₁ $ idealProp r ix
  idealʳ : (r : A) {x : A} (ix : I x) → (∙ x r) ∈ I
  idealʳ r {x} ix = proj₂ $ idealProp r ix
  
  open IsRing isRing public
  open IsSubGroup isSubGroup --public  jak otworzyć tylko te publicznie?
    renaming
    ( ∙_isSubStructure to +_isSubStructure
    ; εInSubset to 0InI
    ; ⁻¹_isSubStructure to ⁻¹_isSubStructure
    ; ≈_respect to ≈_respect
    )

record Ideal c p ℓ : Set (suc (c ⊔ ℓ ⊔ p)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    I       : Pred Carrier p
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isIdeal : IsIdeal I _≈_ _+_ _*_ -_ 0# 1#

  open IsIdeal isIdeal public
  ring : Ring _ _
  ring = record {isRing = isRing}
  
  open Ring ring 


-- jeśli f jest homomorfizmem między pierścieniami to `ker f` jest ideałem.
-- jądro odwzorowania w książce  zapisane jako `ker f = f⁻¹(0)` -- zakładam że chodzi o element neutralny działani addytywnego
kerₕ-ideal : { c₁ c₂ ℓ₁ ℓ₂ : Level} 
  (r₁ : Ring c₁ ℓ₁) (r₂ : Ring c₂ ℓ₂) → let open Ring in
  (f :  Definitions.Morphism (r₁. Carrier) (r₂. Carrier) (r₂. _≈_)) →
  (iRm : IsRingMorphism r₁ r₂ f)
  → let open IsRingMorphism iRm in let
       kern = Kernₕ (IsAbelianGroupMorphism.gp-homo +-abgp-homo)
     in IsIdeal kern (r₁. _≈_) (r₁. _+_) (r₁. _*_) (r₁. -_) (r₁. 0#) (r₁. 1#)
kerₕ-ideal r₁ r₂ f iRm = let open Ring in let open IsRingMorphism iRm in let
   groupMorphism = IsAbelianGroupMorphism.gp-homo +-abgp-homo
   monoidMorphism = IsGroupMorphism.mn-homo groupMorphism
   smMorphism = IsMonoidMorphism.sm-homo monoidMorphism
   semi*Morphism = IsMonoidMorphism.sm-homo *-mn-homo
   kern = Kernₕ groupMorphism
   abelian₁ = +-abelianGroup r₁
   group₁ = AbelianGroup.group abelian₁
   group₂ = AbelianGroup.group (+-abelianGroup r₂)
   isSubGroup : IsSubGroup (r₁ ._≈_) kern (r₁ ._+_) (r₁ .0#) (r₁ .-_)
   isSubGroup  = kernₕ-induces-subgroup groupMorphism
   ideal : (r : (r₁. Carrier)) {x : (r₁. Carrier)} (ix : kern x) → IdealProp kern (r₁ ._*_) r x ix
   ideal r {x} ix = let open EqR (setoid r₂) in let
     frx≈0 : (r₂. _≈_) (f ((r₁. _*_) r x)) (r₂. 0#)
     frx≈0 = begin
       f ((r₁. _*_) r x) ≈⟨ IsSemigroupMorphism.∙-homo semi*Morphism r x ⟩
       (r₂. _*_) (f r) (f x) ≈⟨ (r₂. *-cong) (r₂. refl) ix ⟩ 
       (r₂. _*_) (f r) (r₂. 0#) ≈⟨ zeroʳ r₂ _ ⟩
       (r₂. 0#) ∎
     fxr≈0 : (r₂. _≈_) (f ((r₁. _*_) x r)) (r₂. 0#)
     fxr≈0 = begin
       f ((r₁. _*_) x r) ≈⟨ IsSemigroupMorphism.∙-homo semi*Morphism x r ⟩
       (r₂. _*_) (f x) (f r) ≈⟨ (r₂. *-cong) ix (r₂. refl) ⟩ 
       (r₂. _*_) (r₂. 0#) (f r) ≈⟨ zeroˡ r₂ _ ⟩
       (r₂. 0#) ∎
    in frx≈0 , fxr≈0
 in record { isRing = r₁. isRing ; isSubGroup = isSubGroup ; idealProp = ideal }

record IsSubRing {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (I : Pred A b) (+ ∙ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ b ⊔ ℓ) where
  field
    isRing : IsRing _≈_ + ∙ -_ 0# 1#
    isSub+AbelianGroup : IsSubAbelianGroup _≈_ I + 0# -_
    isSub∙Monoid : IsSubMonoid _≈_ I ∙ 1#

record SubRing c b ℓ : Set (suc (c ⊔ b ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    I       : Pred Carrier b
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isSubRing  : IsSubRing _≈_ I _+_ _*_ -_ 0# 1#

  open IsSubRing isSubRing public

  ring : Ring _ _
  ring = record {isRing = isRing}


{-- str 53:
If I is a two-sided ideal of the ring R, then
multiplication is a function on the quotient group R/I, so R/I is a ring.
--}
module _ {c p ℓ : Level} (ideal : Ideal c p ℓ) where
  open Ideal ideal
  module _ where
    quotientRelation : Rel Carrier p
    quotientRelation = QuotientRelation Carrier I _+_ (-_)
    _≈ₕ_ = quotientRelation
    +-abelian = Ring.+-abelianGroup ring
    +-group = AbelianGroup.group +-abelian
    *-monoid = Ring.*-monoid ring
    isQuotientGroup : IsGroup quotientRelation _+_ 0# (-_)
    isQuotientGroup = quotientGroupIsAGroup +-group I
      (everySubGroupOfAbelianIsNormal +-abelian I isSubGroup)
  open import Algebra.Properties.Ring ring
  R/I-isRing : IsRing quotientRelation _+_ (_*_) (-_) 0# 1#
  R/I-isRing = let open EqR setoid in let
      I∋through0≈ : {x : Carrier} →  (0# ≈ x) → (x ∈ I)  
      I∋through0≈ proof = (IsSubGroup.≈_respect isSubGroup) proof (IsSubGroup.εInSubset isSubGroup)
      comm+ : (x y : Carrier) → ((x + y) + (-(y + x))) ∈ I
      comm+ x y = I∋through0≈ ( begin
        0#  ≈⟨ sym $ AbelianGroup.inverseʳ +-abelian _  ⟩
        (y + x) + -(y + x) ≈⟨ (AbelianGroup.∙-cong +-abelian) (AbelianGroup.comm +-abelian _ _) refl ⟩ 
        (x + y) + -(y + x) ∎)
      quotientLeft*Identity : (x : Carrier) → (1# * x) + - x ∈ I
      quotientLeft*Identity x = I∋through0≈ (begin
        0#  ≈⟨ sym $ AbelianGroup.inverseʳ +-abelian _ ⟩
        x + - x ≈⟨ (AbelianGroup.∙-cong +-abelian) (sym $ Monoid.identityˡ *-monoid x) refl ⟩
        (1# * x) + - x ∎)
      quotientRight*Identity : (x : Carrier) → (x * 1#) + - x ∈ I
      quotientRight*Identity x = I∋through0≈ (begin
        0#  ≈⟨ sym $ AbelianGroup.inverseʳ +-abelian _ ⟩
        x + - x ≈⟨ (AbelianGroup.∙-cong +-abelian) (sym $ Monoid.identityʳ *-monoid x) refl ⟩
        (x * 1#) + - x ∎)
      *ₕ-assoc : (x y z : Carrier) → ((x * y) * z) + - (x * (y * z)) ∈ I
      *ₕ-assoc x y z = I∋through0≈ (begin
        0#  ≈⟨ sym $ AbelianGroup.inverseʳ +-abelian _ ⟩
        (x * (y * z)) + - (x * (y * z)) ≈⟨ (AbelianGroup.∙-cong +-abelian) (sym $ Monoid.assoc *-monoid _ _ _) refl ⟩
        ((x * y) * z) + - (x * (y * z)) ∎)
      *ₕ-cong : ∀ {x y u v} → x + - y ∈ I → u + - v ∈ I → (x * u) + -(y * v) ∈ I
      {-- 
        Plan jest taki:
        x - y ∈ I
        ideał ⇒ xu -yu ∈ I
        u - v ∈ I
        ideał ⇒ yu - yv ∈ I
        podgrupa ⇒ xu - yu + yu - yv ∈ I
        xu -yv ∈ I
      --}
      *ₕ-cong {x} {y} {u} {v} x≈ₕy u≈ₕv = let
        x-y*u : (x + - y) * u ∈ I
        x-y*u = idealʳ u x≈ₕy
        y*u-v : y * (u + - v) ∈ I
        y*u-v = idealˡ y u≈ₕv
        distribˡ = proj₁ $ distrib
        distribʳ = proj₂ $ distrib
        x-y*u≈xu-yu : (x + - y) * u ≈ x * u - (y * u)
        x-y*u≈xu-yu = begin
          (x + - y) * u ≈⟨ distribʳ _ _ _ ⟩
          x * u + (- y) * u ≈⟨ +-cong refl (-‿*-distribˡ _ _) ⟩
          x * u + - (y * u) ∎
        y*u-v≈yu-yv : y * (u + - v) ≈ y * u - (y * v)
        y*u-v≈yu-yv = begin
          y * (u + - v) ≈⟨ distribˡ y u (- v) ⟩
          y * u + y * - v ≈⟨ +-cong refl (-‿*-distribʳ _ _) ⟩
          y * u - (y * v) ∎
        I∋sum : x * u - (y * u) + y * u - (y * v) ∈ I
        I∋sum = IsSubGroup.∙_isSubStructure isSubGroup
          (IsSubGroup.≈_respect isSubGroup x-y*u≈xu-yu x-y*u)
          (IsSubGroup.≈_respect isSubGroup y*u-v≈yu-yv y*u-v)
        in IsSubGroup.≈_respect isSubGroup (begin
             x * u - (y * u) + y * u - (y * v) ≈⟨ sym $ +-assoc _ _ _ ⟩
             x * u - (y * u) + y * u + - (y * v) ≈⟨ +-cong (+-assoc _ _ _) refl ⟩
             x * u + (- (y * u) + y * u) + - (y * v) ≈⟨ +-assoc _ _ _ ⟩
             x * u + (- (y * u) + y * u) - (y * v) ≈⟨ +-cong refl (+-cong (AbelianGroup.inverseˡ +-abelian (y * u)) refl) ⟩
             x * u + 0# - (y * v) ≈⟨ +-cong refl (+-identityˡ _) ⟩
             x * u + - (y * v) ∎)
           I∋sum
      *ₕ-isSemiGroup : IsSemigroup _≈ₕ_ _*_
      *ₕ-isSemiGroup = record { isMagma = record {isEquivalence = IsGroup.isEquivalence isQuotientGroup ; ∙-cong = *ₕ-cong } ; assoc = *ₕ-assoc }
      *ₕ-isMonoid : Algebra.Structures.IsMonoid _≈ₕ_ _*_ 1#
      *ₕ-isMonoid = record { isSemigroup = *ₕ-isSemiGroup ; identity = quotientLeft*Identity , quotientRight*Identity }
      distribₕˡ : ∀ x y z → (x * (y + z)) + - ((x * y) + (x * z)) ∈ I
      distribₕˡ x y z = I∋through0≈ (begin
        0#  ≈⟨ sym $ AbelianGroup.inverseʳ +-abelian _ ⟩
        ((x * y) + (x * z)) + - ((x * y) + (x * z))  ≈⟨ (AbelianGroup.∙-cong +-abelian) (sym $ distribˡ x y z) refl ⟩
        (x * (y + z)) + - ((x * y) + (x * z)) ∎)
      distribₕʳ : ∀ x y z → ((y + z) * x) + - ((y * x) + (z * x)) ∈ I
      distribₕʳ x y z = I∋through0≈ (begin
        0#  ≈⟨ sym $ AbelianGroup.inverseʳ +-abelian _ ⟩
        ((y * x) + (z * x)) + - ((y * x) + (z * x))  ≈⟨ (AbelianGroup.∙-cong +-abelian) (sym $ distribʳ x y z) refl ⟩
        ((y + z) * x) + - ((y * x) + (z * x)) ∎)
    in
      record { +-isAbelianGroup = record { isGroup = isQuotientGroup ; comm = comm+ } ; *-isMonoid = *ₕ-isMonoid ; distrib = distribₕˡ , distribₕʳ }
